So thank you for coming. Good afternoon. It's for me a great pleasure to introduce to you

Professor Michael Colaster. He's a professor at our university in computer science. His

broad field of interest is knowledge management and his talk will be precisely about how mathematics

and computer science interact but maybe not in the way we are used to. We are used to think

on computers as probably support machines in order to help us on computer assisted groups.

But I think we will tell us about some of them. We are very glad that he accepted to deliver this

talk. We tried to promote this series of modules initiated by the Center of Mathematics of Data

University. Other than those that are willing to come here in a dark afternoon, probably also

some of the people will be with us online. You are all very welcome. So thank you Michael.

Thank you.

Let me first disclose that I'm basically by early training genetically predisposed towards math.

Math is the first academic love in my life. But then at some point I got hooked on AI

which with what I mean not machine learning but symbolic AI or as other people say good

old-fashioned AI also termed go fly. So what I want to tell you about today,

I like to start my thoughts with the conclusion. For two reasons. One is I sometimes run out of time.

When I give you the conclusion up front, then after this slide the talk is finished formally.

I cannot run out of time. You probably can ask questions which is at least as important as

getting through the slides. That's why you're seeing the conclusion slide at the beginning.

What I want you to want to tell me about and what the conclusion actually talks is about

formalized mathematics. Formalized mathematics is a topic that has been going on for

60, 70 years by now, almost 70, and mostly unnoticed by mathematicians.

What we do is we express the mathematical knowledge in logic. Then we use sophisticated

software systems like what we call proof systems that actually verify or compute and support our

management of this mathematical knowledge. In particular, check proofs. We have what we call

the calculus, a logical system, comes with a way of making proofs. It's so explicit that a machine

can actually check it and at the end say, yeah, we have a proof. Then we really do have a proof.

It doesn't have any gaps because the proof assistant checker is dumb. It doesn't fill any

gaps. It doesn't want to fill any gaps like we as mathematicians do. We never write down the whole

proof. We always leave out data, details because our readers can reconstruct them. Except sometimes

there isn't really a proof gap to be filled. It's just a mistake. Proof assistants

are very, very meticulous about this. If a proof assistant says we have a proof, we actually do

have a proof. It's gory detail. It may be a terabyte long, the proof. Nobody would want to read it.

It's difficult to learn anything from it, but we have a proof. It's a certificate, much less than

what we as mathematicians think of as a proof, which is a conversational piece made for convincing

others of the truth of something and showing them the nice level, the nice techniques I've invented

in the course of this. We also make modular libraries of reusable mathematical components

in the process. That's kind of what I was tasked to do. I mentioned formalized mathematics in a

meeting and I got to, you have to give us a talk about it. This sounds nice. That's kind of the

thing I'm supposed to deliver. It's not really what I do in my research. In my research, we try to

get around the problems that this makes. One of the things that we're going to see is that

full formalization and full formalization of proof is extremely, extremely tedious.

You don't really want to do it, but there's a heavyweight method. They give you full truth assurance.

But there's not really anything wrong with peer review. Thank you very much. If there is an error,

it will be found. Or the paper is irrelevant anyway, then nobody reads it and nobody finds

the bugs, but nobody cares about the bugs either. I would like to show you, if we have time and

you're not asking so many questions, to show you a couple of more lightweight things like formula

search and how one could do that, or taking latex papers and extracting semantics out of those.

And I think of those as not fully formal, but maths doing flexible formulas.

And if we have time, there's another facet of this where instead of talking about one logic for

what theorem prover, we kind of try to connect all of them and all of those. I know this is